(0) Obligation:
Clauses:
t(N) :- ','(ll(N, Xs), ','(select(X1, Xs, Xs1), ','(ll(M, Xs1), t(M)))).
t(0).
ll(s(N), .(X, Xs)) :- ll(N, Xs).
ll(0, []).
select(X, .(Y, Xs), .(Y, Ys)) :- select(X, Xs, Ys).
select(X, .(X, Xs), Xs).
Query: t(g)
(1) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph DT10.
(2) Obligation:
Triples:
llA(s(X1), .(X2, X3)) :- llA(X1, X3).
selectB(X1, .(X2, X3), .(X2, X4)) :- selectB(X1, X3, X4).
llE(s(X1), .(X2, X3)) :- llE(X1, X3).
llG(s(X1), .(X2, X3)) :- llG(X1, X3).
tC(s(X1)) :- llA(X1, X2).
tC(s(X1)) :- ','(llcA(X1, X2), selectB(X3, X2, X4)).
tC(s(X1)) :- ','(llcA(X1, X2), ','(selectcD(X3, X4, X2, X5), llE(X6, X5))).
tC(s(X1)) :- ','(llcA(X1, X2), ','(selectcD(X3, X4, X2, X5), ','(llcE(X6, X5), tC(X6)))).
tC(0) :- ','(selectcF(X1, X2), llG(X3, X2)).
tC(0) :- ','(selectcF(X1, X2), ','(llcG(X3, X2), tC(X3))).
Clauses:
llcA(s(X1), .(X2, X3)) :- llcA(X1, X3).
llcA(0, []).
selectcB(X1, .(X2, X3), .(X2, X4)) :- selectcB(X1, X3, X4).
selectcB(X1, .(X1, X2), X2).
tcC(s(X1)) :- ','(llcA(X1, X2), ','(selectcD(X3, X4, X2, X5), ','(llcE(X6, X5), tcC(X6)))).
tcC(0) :- ','(selectcF(X1, X2), ','(llcG(X3, X2), tcC(X3))).
tcC(0).
llcE(s(X1), .(X2, X3)) :- llcE(X1, X3).
llcE(0, []).
llcG(s(X1), .(X2, X3)) :- llcG(X1, X3).
llcG(0, []).
selectcD(X1, X2, X3, .(X2, X4)) :- selectcB(X1, X3, X4).
selectcD(X1, X1, X2, X2).
Afs:
tC(x1) = tC(x1)
(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)
Deleted triples and predicates having undefined goals [DT09].
(4) Obligation:
Triples:
llA(s(X1), .(X2, X3)) :- llA(X1, X3).
selectB(X1, .(X2, X3), .(X2, X4)) :- selectB(X1, X3, X4).
llE(s(X1), .(X2, X3)) :- llE(X1, X3).
llG(s(X1), .(X2, X3)) :- llG(X1, X3).
tC(s(X1)) :- llA(X1, X2).
tC(s(X1)) :- ','(llcA(X1, X2), selectB(X3, X2, X4)).
tC(s(X1)) :- ','(llcA(X1, X2), ','(selectcD(X3, X4, X2, X5), llE(X6, X5))).
tC(s(X1)) :- ','(llcA(X1, X2), ','(selectcD(X3, X4, X2, X5), ','(llcE(X6, X5), tC(X6)))).
Clauses:
llcA(s(X1), .(X2, X3)) :- llcA(X1, X3).
llcA(0, []).
selectcB(X1, .(X2, X3), .(X2, X4)) :- selectcB(X1, X3, X4).
selectcB(X1, .(X1, X2), X2).
tcC(s(X1)) :- ','(llcA(X1, X2), ','(selectcD(X3, X4, X2, X5), ','(llcE(X6, X5), tcC(X6)))).
tcC(0).
llcE(s(X1), .(X2, X3)) :- llcE(X1, X3).
llcE(0, []).
llcG(s(X1), .(X2, X3)) :- llcG(X1, X3).
llcG(0, []).
selectcD(X1, X2, X3, .(X2, X4)) :- selectcB(X1, X3, X4).
selectcD(X1, X1, X2, X2).
Afs:
tC(x1) = tC(x1)
(5) TriplesToPiDPProof (SOUND transformation)
We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
tC_in: (b)
llA_in: (b,f)
llcA_in: (b,f)
selectB_in: (f,b,f)
selectcD_in: (f,f,b,f)
selectcB_in: (f,b,f)
llE_in: (f,b)
llcE_in: (f,b)
Transforming
TRIPLES into the following
Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:
TC_IN_G(s(X1)) → U5_G(X1, llA_in_ga(X1, X2))
TC_IN_G(s(X1)) → LLA_IN_GA(X1, X2)
LLA_IN_GA(s(X1), .(X2, X3)) → U1_GA(X1, X2, X3, llA_in_ga(X1, X3))
LLA_IN_GA(s(X1), .(X2, X3)) → LLA_IN_GA(X1, X3)
TC_IN_G(s(X1)) → U6_G(X1, llcA_in_ga(X1, X2))
U6_G(X1, llcA_out_ga(X1, X2)) → U7_G(X1, selectB_in_aga(X3, X2, X4))
U6_G(X1, llcA_out_ga(X1, X2)) → SELECTB_IN_AGA(X3, X2, X4)
SELECTB_IN_AGA(X1, .(X2, X3), .(X2, X4)) → U2_AGA(X1, X2, X3, X4, selectB_in_aga(X1, X3, X4))
SELECTB_IN_AGA(X1, .(X2, X3), .(X2, X4)) → SELECTB_IN_AGA(X1, X3, X4)
U6_G(X1, llcA_out_ga(X1, X2)) → U8_G(X1, selectcD_in_aaga(X3, X4, X2, X5))
U8_G(X1, selectcD_out_aaga(X3, X4, X2, X5)) → U9_G(X1, llE_in_ag(X6, X5))
U8_G(X1, selectcD_out_aaga(X3, X4, X2, X5)) → LLE_IN_AG(X6, X5)
LLE_IN_AG(s(X1), .(X2, X3)) → U3_AG(X1, X2, X3, llE_in_ag(X1, X3))
LLE_IN_AG(s(X1), .(X2, X3)) → LLE_IN_AG(X1, X3)
U8_G(X1, selectcD_out_aaga(X3, X4, X2, X5)) → U10_G(X1, llcE_in_ag(X6, X5))
U10_G(X1, llcE_out_ag(X6, X5)) → U11_G(X1, tC_in_g(X6))
U10_G(X1, llcE_out_ag(X6, X5)) → TC_IN_G(X6)
The TRS R consists of the following rules:
llcA_in_ga(s(X1), .(X2, X3)) → U13_ga(X1, X2, X3, llcA_in_ga(X1, X3))
llcA_in_ga(0, []) → llcA_out_ga(0, [])
U13_ga(X1, X2, X3, llcA_out_ga(X1, X3)) → llcA_out_ga(s(X1), .(X2, X3))
selectcD_in_aaga(X1, X2, X3, .(X2, X4)) → U21_aaga(X1, X2, X3, X4, selectcB_in_aga(X1, X3, X4))
selectcB_in_aga(X1, .(X2, X3), .(X2, X4)) → U14_aga(X1, X2, X3, X4, selectcB_in_aga(X1, X3, X4))
selectcB_in_aga(X1, .(X1, X2), X2) → selectcB_out_aga(X1, .(X1, X2), X2)
U14_aga(X1, X2, X3, X4, selectcB_out_aga(X1, X3, X4)) → selectcB_out_aga(X1, .(X2, X3), .(X2, X4))
U21_aaga(X1, X2, X3, X4, selectcB_out_aga(X1, X3, X4)) → selectcD_out_aaga(X1, X2, X3, .(X2, X4))
selectcD_in_aaga(X1, X1, X2, X2) → selectcD_out_aaga(X1, X1, X2, X2)
llcE_in_ag(s(X1), .(X2, X3)) → U19_ag(X1, X2, X3, llcE_in_ag(X1, X3))
llcE_in_ag(0, []) → llcE_out_ag(0, [])
U19_ag(X1, X2, X3, llcE_out_ag(X1, X3)) → llcE_out_ag(s(X1), .(X2, X3))
The argument filtering Pi contains the following mapping:
tC_in_g(
x1) =
tC_in_g(
x1)
s(
x1) =
s(
x1)
llA_in_ga(
x1,
x2) =
llA_in_ga(
x1)
.(
x1,
x2) =
.(
x2)
llcA_in_ga(
x1,
x2) =
llcA_in_ga(
x1)
U13_ga(
x1,
x2,
x3,
x4) =
U13_ga(
x1,
x4)
0 =
0
llcA_out_ga(
x1,
x2) =
llcA_out_ga(
x1,
x2)
selectB_in_aga(
x1,
x2,
x3) =
selectB_in_aga(
x2)
selectcD_in_aaga(
x1,
x2,
x3,
x4) =
selectcD_in_aaga(
x3)
U21_aaga(
x1,
x2,
x3,
x4,
x5) =
U21_aaga(
x3,
x5)
selectcB_in_aga(
x1,
x2,
x3) =
selectcB_in_aga(
x2)
U14_aga(
x1,
x2,
x3,
x4,
x5) =
U14_aga(
x3,
x5)
selectcB_out_aga(
x1,
x2,
x3) =
selectcB_out_aga(
x2,
x3)
selectcD_out_aaga(
x1,
x2,
x3,
x4) =
selectcD_out_aaga(
x3,
x4)
llE_in_ag(
x1,
x2) =
llE_in_ag(
x2)
llcE_in_ag(
x1,
x2) =
llcE_in_ag(
x2)
U19_ag(
x1,
x2,
x3,
x4) =
U19_ag(
x3,
x4)
[] =
[]
llcE_out_ag(
x1,
x2) =
llcE_out_ag(
x1,
x2)
TC_IN_G(
x1) =
TC_IN_G(
x1)
U5_G(
x1,
x2) =
U5_G(
x1,
x2)
LLA_IN_GA(
x1,
x2) =
LLA_IN_GA(
x1)
U1_GA(
x1,
x2,
x3,
x4) =
U1_GA(
x1,
x4)
U6_G(
x1,
x2) =
U6_G(
x1,
x2)
U7_G(
x1,
x2) =
U7_G(
x1,
x2)
SELECTB_IN_AGA(
x1,
x2,
x3) =
SELECTB_IN_AGA(
x2)
U2_AGA(
x1,
x2,
x3,
x4,
x5) =
U2_AGA(
x3,
x5)
U8_G(
x1,
x2) =
U8_G(
x1,
x2)
U9_G(
x1,
x2) =
U9_G(
x1,
x2)
LLE_IN_AG(
x1,
x2) =
LLE_IN_AG(
x2)
U3_AG(
x1,
x2,
x3,
x4) =
U3_AG(
x3,
x4)
U10_G(
x1,
x2) =
U10_G(
x1,
x2)
U11_G(
x1,
x2) =
U11_G(
x1,
x2)
We have to consider all (P,R,Pi)-chains
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
(6) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
TC_IN_G(s(X1)) → U5_G(X1, llA_in_ga(X1, X2))
TC_IN_G(s(X1)) → LLA_IN_GA(X1, X2)
LLA_IN_GA(s(X1), .(X2, X3)) → U1_GA(X1, X2, X3, llA_in_ga(X1, X3))
LLA_IN_GA(s(X1), .(X2, X3)) → LLA_IN_GA(X1, X3)
TC_IN_G(s(X1)) → U6_G(X1, llcA_in_ga(X1, X2))
U6_G(X1, llcA_out_ga(X1, X2)) → U7_G(X1, selectB_in_aga(X3, X2, X4))
U6_G(X1, llcA_out_ga(X1, X2)) → SELECTB_IN_AGA(X3, X2, X4)
SELECTB_IN_AGA(X1, .(X2, X3), .(X2, X4)) → U2_AGA(X1, X2, X3, X4, selectB_in_aga(X1, X3, X4))
SELECTB_IN_AGA(X1, .(X2, X3), .(X2, X4)) → SELECTB_IN_AGA(X1, X3, X4)
U6_G(X1, llcA_out_ga(X1, X2)) → U8_G(X1, selectcD_in_aaga(X3, X4, X2, X5))
U8_G(X1, selectcD_out_aaga(X3, X4, X2, X5)) → U9_G(X1, llE_in_ag(X6, X5))
U8_G(X1, selectcD_out_aaga(X3, X4, X2, X5)) → LLE_IN_AG(X6, X5)
LLE_IN_AG(s(X1), .(X2, X3)) → U3_AG(X1, X2, X3, llE_in_ag(X1, X3))
LLE_IN_AG(s(X1), .(X2, X3)) → LLE_IN_AG(X1, X3)
U8_G(X1, selectcD_out_aaga(X3, X4, X2, X5)) → U10_G(X1, llcE_in_ag(X6, X5))
U10_G(X1, llcE_out_ag(X6, X5)) → U11_G(X1, tC_in_g(X6))
U10_G(X1, llcE_out_ag(X6, X5)) → TC_IN_G(X6)
The TRS R consists of the following rules:
llcA_in_ga(s(X1), .(X2, X3)) → U13_ga(X1, X2, X3, llcA_in_ga(X1, X3))
llcA_in_ga(0, []) → llcA_out_ga(0, [])
U13_ga(X1, X2, X3, llcA_out_ga(X1, X3)) → llcA_out_ga(s(X1), .(X2, X3))
selectcD_in_aaga(X1, X2, X3, .(X2, X4)) → U21_aaga(X1, X2, X3, X4, selectcB_in_aga(X1, X3, X4))
selectcB_in_aga(X1, .(X2, X3), .(X2, X4)) → U14_aga(X1, X2, X3, X4, selectcB_in_aga(X1, X3, X4))
selectcB_in_aga(X1, .(X1, X2), X2) → selectcB_out_aga(X1, .(X1, X2), X2)
U14_aga(X1, X2, X3, X4, selectcB_out_aga(X1, X3, X4)) → selectcB_out_aga(X1, .(X2, X3), .(X2, X4))
U21_aaga(X1, X2, X3, X4, selectcB_out_aga(X1, X3, X4)) → selectcD_out_aaga(X1, X2, X3, .(X2, X4))
selectcD_in_aaga(X1, X1, X2, X2) → selectcD_out_aaga(X1, X1, X2, X2)
llcE_in_ag(s(X1), .(X2, X3)) → U19_ag(X1, X2, X3, llcE_in_ag(X1, X3))
llcE_in_ag(0, []) → llcE_out_ag(0, [])
U19_ag(X1, X2, X3, llcE_out_ag(X1, X3)) → llcE_out_ag(s(X1), .(X2, X3))
The argument filtering Pi contains the following mapping:
tC_in_g(
x1) =
tC_in_g(
x1)
s(
x1) =
s(
x1)
llA_in_ga(
x1,
x2) =
llA_in_ga(
x1)
.(
x1,
x2) =
.(
x2)
llcA_in_ga(
x1,
x2) =
llcA_in_ga(
x1)
U13_ga(
x1,
x2,
x3,
x4) =
U13_ga(
x1,
x4)
0 =
0
llcA_out_ga(
x1,
x2) =
llcA_out_ga(
x1,
x2)
selectB_in_aga(
x1,
x2,
x3) =
selectB_in_aga(
x2)
selectcD_in_aaga(
x1,
x2,
x3,
x4) =
selectcD_in_aaga(
x3)
U21_aaga(
x1,
x2,
x3,
x4,
x5) =
U21_aaga(
x3,
x5)
selectcB_in_aga(
x1,
x2,
x3) =
selectcB_in_aga(
x2)
U14_aga(
x1,
x2,
x3,
x4,
x5) =
U14_aga(
x3,
x5)
selectcB_out_aga(
x1,
x2,
x3) =
selectcB_out_aga(
x2,
x3)
selectcD_out_aaga(
x1,
x2,
x3,
x4) =
selectcD_out_aaga(
x3,
x4)
llE_in_ag(
x1,
x2) =
llE_in_ag(
x2)
llcE_in_ag(
x1,
x2) =
llcE_in_ag(
x2)
U19_ag(
x1,
x2,
x3,
x4) =
U19_ag(
x3,
x4)
[] =
[]
llcE_out_ag(
x1,
x2) =
llcE_out_ag(
x1,
x2)
TC_IN_G(
x1) =
TC_IN_G(
x1)
U5_G(
x1,
x2) =
U5_G(
x1,
x2)
LLA_IN_GA(
x1,
x2) =
LLA_IN_GA(
x1)
U1_GA(
x1,
x2,
x3,
x4) =
U1_GA(
x1,
x4)
U6_G(
x1,
x2) =
U6_G(
x1,
x2)
U7_G(
x1,
x2) =
U7_G(
x1,
x2)
SELECTB_IN_AGA(
x1,
x2,
x3) =
SELECTB_IN_AGA(
x2)
U2_AGA(
x1,
x2,
x3,
x4,
x5) =
U2_AGA(
x3,
x5)
U8_G(
x1,
x2) =
U8_G(
x1,
x2)
U9_G(
x1,
x2) =
U9_G(
x1,
x2)
LLE_IN_AG(
x1,
x2) =
LLE_IN_AG(
x2)
U3_AG(
x1,
x2,
x3,
x4) =
U3_AG(
x3,
x4)
U10_G(
x1,
x2) =
U10_G(
x1,
x2)
U11_G(
x1,
x2) =
U11_G(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(7) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 10 less nodes.
(8) Complex Obligation (AND)
(9) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
LLE_IN_AG(s(X1), .(X2, X3)) → LLE_IN_AG(X1, X3)
The TRS R consists of the following rules:
llcA_in_ga(s(X1), .(X2, X3)) → U13_ga(X1, X2, X3, llcA_in_ga(X1, X3))
llcA_in_ga(0, []) → llcA_out_ga(0, [])
U13_ga(X1, X2, X3, llcA_out_ga(X1, X3)) → llcA_out_ga(s(X1), .(X2, X3))
selectcD_in_aaga(X1, X2, X3, .(X2, X4)) → U21_aaga(X1, X2, X3, X4, selectcB_in_aga(X1, X3, X4))
selectcB_in_aga(X1, .(X2, X3), .(X2, X4)) → U14_aga(X1, X2, X3, X4, selectcB_in_aga(X1, X3, X4))
selectcB_in_aga(X1, .(X1, X2), X2) → selectcB_out_aga(X1, .(X1, X2), X2)
U14_aga(X1, X2, X3, X4, selectcB_out_aga(X1, X3, X4)) → selectcB_out_aga(X1, .(X2, X3), .(X2, X4))
U21_aaga(X1, X2, X3, X4, selectcB_out_aga(X1, X3, X4)) → selectcD_out_aaga(X1, X2, X3, .(X2, X4))
selectcD_in_aaga(X1, X1, X2, X2) → selectcD_out_aaga(X1, X1, X2, X2)
llcE_in_ag(s(X1), .(X2, X3)) → U19_ag(X1, X2, X3, llcE_in_ag(X1, X3))
llcE_in_ag(0, []) → llcE_out_ag(0, [])
U19_ag(X1, X2, X3, llcE_out_ag(X1, X3)) → llcE_out_ag(s(X1), .(X2, X3))
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
.(
x1,
x2) =
.(
x2)
llcA_in_ga(
x1,
x2) =
llcA_in_ga(
x1)
U13_ga(
x1,
x2,
x3,
x4) =
U13_ga(
x1,
x4)
0 =
0
llcA_out_ga(
x1,
x2) =
llcA_out_ga(
x1,
x2)
selectcD_in_aaga(
x1,
x2,
x3,
x4) =
selectcD_in_aaga(
x3)
U21_aaga(
x1,
x2,
x3,
x4,
x5) =
U21_aaga(
x3,
x5)
selectcB_in_aga(
x1,
x2,
x3) =
selectcB_in_aga(
x2)
U14_aga(
x1,
x2,
x3,
x4,
x5) =
U14_aga(
x3,
x5)
selectcB_out_aga(
x1,
x2,
x3) =
selectcB_out_aga(
x2,
x3)
selectcD_out_aaga(
x1,
x2,
x3,
x4) =
selectcD_out_aaga(
x3,
x4)
llcE_in_ag(
x1,
x2) =
llcE_in_ag(
x2)
U19_ag(
x1,
x2,
x3,
x4) =
U19_ag(
x3,
x4)
[] =
[]
llcE_out_ag(
x1,
x2) =
llcE_out_ag(
x1,
x2)
LLE_IN_AG(
x1,
x2) =
LLE_IN_AG(
x2)
We have to consider all (P,R,Pi)-chains
(10) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(11) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
LLE_IN_AG(s(X1), .(X2, X3)) → LLE_IN_AG(X1, X3)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
.(
x1,
x2) =
.(
x2)
LLE_IN_AG(
x1,
x2) =
LLE_IN_AG(
x2)
We have to consider all (P,R,Pi)-chains
(12) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(13) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LLE_IN_AG(.(X3)) → LLE_IN_AG(X3)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(14) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- LLE_IN_AG(.(X3)) → LLE_IN_AG(X3)
The graph contains the following edges 1 > 1
(15) YES
(16) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
SELECTB_IN_AGA(X1, .(X2, X3), .(X2, X4)) → SELECTB_IN_AGA(X1, X3, X4)
The TRS R consists of the following rules:
llcA_in_ga(s(X1), .(X2, X3)) → U13_ga(X1, X2, X3, llcA_in_ga(X1, X3))
llcA_in_ga(0, []) → llcA_out_ga(0, [])
U13_ga(X1, X2, X3, llcA_out_ga(X1, X3)) → llcA_out_ga(s(X1), .(X2, X3))
selectcD_in_aaga(X1, X2, X3, .(X2, X4)) → U21_aaga(X1, X2, X3, X4, selectcB_in_aga(X1, X3, X4))
selectcB_in_aga(X1, .(X2, X3), .(X2, X4)) → U14_aga(X1, X2, X3, X4, selectcB_in_aga(X1, X3, X4))
selectcB_in_aga(X1, .(X1, X2), X2) → selectcB_out_aga(X1, .(X1, X2), X2)
U14_aga(X1, X2, X3, X4, selectcB_out_aga(X1, X3, X4)) → selectcB_out_aga(X1, .(X2, X3), .(X2, X4))
U21_aaga(X1, X2, X3, X4, selectcB_out_aga(X1, X3, X4)) → selectcD_out_aaga(X1, X2, X3, .(X2, X4))
selectcD_in_aaga(X1, X1, X2, X2) → selectcD_out_aaga(X1, X1, X2, X2)
llcE_in_ag(s(X1), .(X2, X3)) → U19_ag(X1, X2, X3, llcE_in_ag(X1, X3))
llcE_in_ag(0, []) → llcE_out_ag(0, [])
U19_ag(X1, X2, X3, llcE_out_ag(X1, X3)) → llcE_out_ag(s(X1), .(X2, X3))
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
.(
x1,
x2) =
.(
x2)
llcA_in_ga(
x1,
x2) =
llcA_in_ga(
x1)
U13_ga(
x1,
x2,
x3,
x4) =
U13_ga(
x1,
x4)
0 =
0
llcA_out_ga(
x1,
x2) =
llcA_out_ga(
x1,
x2)
selectcD_in_aaga(
x1,
x2,
x3,
x4) =
selectcD_in_aaga(
x3)
U21_aaga(
x1,
x2,
x3,
x4,
x5) =
U21_aaga(
x3,
x5)
selectcB_in_aga(
x1,
x2,
x3) =
selectcB_in_aga(
x2)
U14_aga(
x1,
x2,
x3,
x4,
x5) =
U14_aga(
x3,
x5)
selectcB_out_aga(
x1,
x2,
x3) =
selectcB_out_aga(
x2,
x3)
selectcD_out_aaga(
x1,
x2,
x3,
x4) =
selectcD_out_aaga(
x3,
x4)
llcE_in_ag(
x1,
x2) =
llcE_in_ag(
x2)
U19_ag(
x1,
x2,
x3,
x4) =
U19_ag(
x3,
x4)
[] =
[]
llcE_out_ag(
x1,
x2) =
llcE_out_ag(
x1,
x2)
SELECTB_IN_AGA(
x1,
x2,
x3) =
SELECTB_IN_AGA(
x2)
We have to consider all (P,R,Pi)-chains
(17) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(18) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
SELECTB_IN_AGA(X1, .(X2, X3), .(X2, X4)) → SELECTB_IN_AGA(X1, X3, X4)
R is empty.
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x2)
SELECTB_IN_AGA(
x1,
x2,
x3) =
SELECTB_IN_AGA(
x2)
We have to consider all (P,R,Pi)-chains
(19) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(20) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SELECTB_IN_AGA(.(X3)) → SELECTB_IN_AGA(X3)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(21) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- SELECTB_IN_AGA(.(X3)) → SELECTB_IN_AGA(X3)
The graph contains the following edges 1 > 1
(22) YES
(23) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
LLA_IN_GA(s(X1), .(X2, X3)) → LLA_IN_GA(X1, X3)
The TRS R consists of the following rules:
llcA_in_ga(s(X1), .(X2, X3)) → U13_ga(X1, X2, X3, llcA_in_ga(X1, X3))
llcA_in_ga(0, []) → llcA_out_ga(0, [])
U13_ga(X1, X2, X3, llcA_out_ga(X1, X3)) → llcA_out_ga(s(X1), .(X2, X3))
selectcD_in_aaga(X1, X2, X3, .(X2, X4)) → U21_aaga(X1, X2, X3, X4, selectcB_in_aga(X1, X3, X4))
selectcB_in_aga(X1, .(X2, X3), .(X2, X4)) → U14_aga(X1, X2, X3, X4, selectcB_in_aga(X1, X3, X4))
selectcB_in_aga(X1, .(X1, X2), X2) → selectcB_out_aga(X1, .(X1, X2), X2)
U14_aga(X1, X2, X3, X4, selectcB_out_aga(X1, X3, X4)) → selectcB_out_aga(X1, .(X2, X3), .(X2, X4))
U21_aaga(X1, X2, X3, X4, selectcB_out_aga(X1, X3, X4)) → selectcD_out_aaga(X1, X2, X3, .(X2, X4))
selectcD_in_aaga(X1, X1, X2, X2) → selectcD_out_aaga(X1, X1, X2, X2)
llcE_in_ag(s(X1), .(X2, X3)) → U19_ag(X1, X2, X3, llcE_in_ag(X1, X3))
llcE_in_ag(0, []) → llcE_out_ag(0, [])
U19_ag(X1, X2, X3, llcE_out_ag(X1, X3)) → llcE_out_ag(s(X1), .(X2, X3))
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
.(
x1,
x2) =
.(
x2)
llcA_in_ga(
x1,
x2) =
llcA_in_ga(
x1)
U13_ga(
x1,
x2,
x3,
x4) =
U13_ga(
x1,
x4)
0 =
0
llcA_out_ga(
x1,
x2) =
llcA_out_ga(
x1,
x2)
selectcD_in_aaga(
x1,
x2,
x3,
x4) =
selectcD_in_aaga(
x3)
U21_aaga(
x1,
x2,
x3,
x4,
x5) =
U21_aaga(
x3,
x5)
selectcB_in_aga(
x1,
x2,
x3) =
selectcB_in_aga(
x2)
U14_aga(
x1,
x2,
x3,
x4,
x5) =
U14_aga(
x3,
x5)
selectcB_out_aga(
x1,
x2,
x3) =
selectcB_out_aga(
x2,
x3)
selectcD_out_aaga(
x1,
x2,
x3,
x4) =
selectcD_out_aaga(
x3,
x4)
llcE_in_ag(
x1,
x2) =
llcE_in_ag(
x2)
U19_ag(
x1,
x2,
x3,
x4) =
U19_ag(
x3,
x4)
[] =
[]
llcE_out_ag(
x1,
x2) =
llcE_out_ag(
x1,
x2)
LLA_IN_GA(
x1,
x2) =
LLA_IN_GA(
x1)
We have to consider all (P,R,Pi)-chains
(24) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(25) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
LLA_IN_GA(s(X1), .(X2, X3)) → LLA_IN_GA(X1, X3)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
.(
x1,
x2) =
.(
x2)
LLA_IN_GA(
x1,
x2) =
LLA_IN_GA(
x1)
We have to consider all (P,R,Pi)-chains
(26) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(27) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LLA_IN_GA(s(X1)) → LLA_IN_GA(X1)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(28) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- LLA_IN_GA(s(X1)) → LLA_IN_GA(X1)
The graph contains the following edges 1 > 1
(29) YES
(30) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
TC_IN_G(s(X1)) → U6_G(X1, llcA_in_ga(X1, X2))
U6_G(X1, llcA_out_ga(X1, X2)) → U8_G(X1, selectcD_in_aaga(X3, X4, X2, X5))
U8_G(X1, selectcD_out_aaga(X3, X4, X2, X5)) → U10_G(X1, llcE_in_ag(X6, X5))
U10_G(X1, llcE_out_ag(X6, X5)) → TC_IN_G(X6)
The TRS R consists of the following rules:
llcA_in_ga(s(X1), .(X2, X3)) → U13_ga(X1, X2, X3, llcA_in_ga(X1, X3))
llcA_in_ga(0, []) → llcA_out_ga(0, [])
U13_ga(X1, X2, X3, llcA_out_ga(X1, X3)) → llcA_out_ga(s(X1), .(X2, X3))
selectcD_in_aaga(X1, X2, X3, .(X2, X4)) → U21_aaga(X1, X2, X3, X4, selectcB_in_aga(X1, X3, X4))
selectcB_in_aga(X1, .(X2, X3), .(X2, X4)) → U14_aga(X1, X2, X3, X4, selectcB_in_aga(X1, X3, X4))
selectcB_in_aga(X1, .(X1, X2), X2) → selectcB_out_aga(X1, .(X1, X2), X2)
U14_aga(X1, X2, X3, X4, selectcB_out_aga(X1, X3, X4)) → selectcB_out_aga(X1, .(X2, X3), .(X2, X4))
U21_aaga(X1, X2, X3, X4, selectcB_out_aga(X1, X3, X4)) → selectcD_out_aaga(X1, X2, X3, .(X2, X4))
selectcD_in_aaga(X1, X1, X2, X2) → selectcD_out_aaga(X1, X1, X2, X2)
llcE_in_ag(s(X1), .(X2, X3)) → U19_ag(X1, X2, X3, llcE_in_ag(X1, X3))
llcE_in_ag(0, []) → llcE_out_ag(0, [])
U19_ag(X1, X2, X3, llcE_out_ag(X1, X3)) → llcE_out_ag(s(X1), .(X2, X3))
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
.(
x1,
x2) =
.(
x2)
llcA_in_ga(
x1,
x2) =
llcA_in_ga(
x1)
U13_ga(
x1,
x2,
x3,
x4) =
U13_ga(
x1,
x4)
0 =
0
llcA_out_ga(
x1,
x2) =
llcA_out_ga(
x1,
x2)
selectcD_in_aaga(
x1,
x2,
x3,
x4) =
selectcD_in_aaga(
x3)
U21_aaga(
x1,
x2,
x3,
x4,
x5) =
U21_aaga(
x3,
x5)
selectcB_in_aga(
x1,
x2,
x3) =
selectcB_in_aga(
x2)
U14_aga(
x1,
x2,
x3,
x4,
x5) =
U14_aga(
x3,
x5)
selectcB_out_aga(
x1,
x2,
x3) =
selectcB_out_aga(
x2,
x3)
selectcD_out_aaga(
x1,
x2,
x3,
x4) =
selectcD_out_aaga(
x3,
x4)
llcE_in_ag(
x1,
x2) =
llcE_in_ag(
x2)
U19_ag(
x1,
x2,
x3,
x4) =
U19_ag(
x3,
x4)
[] =
[]
llcE_out_ag(
x1,
x2) =
llcE_out_ag(
x1,
x2)
TC_IN_G(
x1) =
TC_IN_G(
x1)
U6_G(
x1,
x2) =
U6_G(
x1,
x2)
U8_G(
x1,
x2) =
U8_G(
x1,
x2)
U10_G(
x1,
x2) =
U10_G(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(31) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(32) Obligation:
Q DP problem:
The TRS P consists of the following rules:
TC_IN_G(s(X1)) → U6_G(X1, llcA_in_ga(X1))
U6_G(X1, llcA_out_ga(X1, X2)) → U8_G(X1, selectcD_in_aaga(X2))
U8_G(X1, selectcD_out_aaga(X2, X5)) → U10_G(X1, llcE_in_ag(X5))
U10_G(X1, llcE_out_ag(X6, X5)) → TC_IN_G(X6)
The TRS R consists of the following rules:
llcA_in_ga(s(X1)) → U13_ga(X1, llcA_in_ga(X1))
llcA_in_ga(0) → llcA_out_ga(0, [])
U13_ga(X1, llcA_out_ga(X1, X3)) → llcA_out_ga(s(X1), .(X3))
selectcD_in_aaga(X3) → U21_aaga(X3, selectcB_in_aga(X3))
selectcB_in_aga(.(X3)) → U14_aga(X3, selectcB_in_aga(X3))
selectcB_in_aga(.(X2)) → selectcB_out_aga(.(X2), X2)
U14_aga(X3, selectcB_out_aga(X3, X4)) → selectcB_out_aga(.(X3), .(X4))
U21_aaga(X3, selectcB_out_aga(X3, X4)) → selectcD_out_aaga(X3, .(X4))
selectcD_in_aaga(X2) → selectcD_out_aaga(X2, X2)
llcE_in_ag(.(X3)) → U19_ag(X3, llcE_in_ag(X3))
llcE_in_ag([]) → llcE_out_ag(0, [])
U19_ag(X3, llcE_out_ag(X1, X3)) → llcE_out_ag(s(X1), .(X3))
The set Q consists of the following terms:
llcA_in_ga(x0)
U13_ga(x0, x1)
selectcD_in_aaga(x0)
selectcB_in_aga(x0)
U14_aga(x0, x1)
U21_aaga(x0, x1)
llcE_in_ag(x0)
U19_ag(x0, x1)
We have to consider all (P,Q,R)-chains.
(33) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
U6_G(X1, llcA_out_ga(X1, X2)) → U8_G(X1, selectcD_in_aaga(X2))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(.(x1)) = 1 + x1
POL(0) = 0
POL(TC_IN_G(x1)) = x1
POL(U10_G(x1, x2)) = x2
POL(U13_ga(x1, x2)) = 1 + x2
POL(U14_aga(x1, x2)) = 1 + x2
POL(U19_ag(x1, x2)) = 1 + x2
POL(U21_aaga(x1, x2)) = x2
POL(U6_G(x1, x2)) = 1 + x2
POL(U8_G(x1, x2)) = x2
POL([]) = 0
POL(llcA_in_ga(x1)) = x1
POL(llcA_out_ga(x1, x2)) = x2
POL(llcE_in_ag(x1)) = x1
POL(llcE_out_ag(x1, x2)) = x1
POL(s(x1)) = 1 + x1
POL(selectcB_in_aga(x1)) = x1
POL(selectcB_out_aga(x1, x2)) = 1 + x2
POL(selectcD_in_aaga(x1)) = x1
POL(selectcD_out_aaga(x1, x2)) = x2
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
llcA_in_ga(s(X1)) → U13_ga(X1, llcA_in_ga(X1))
llcA_in_ga(0) → llcA_out_ga(0, [])
selectcD_in_aaga(X3) → U21_aaga(X3, selectcB_in_aga(X3))
selectcD_in_aaga(X2) → selectcD_out_aaga(X2, X2)
llcE_in_ag(.(X3)) → U19_ag(X3, llcE_in_ag(X3))
llcE_in_ag([]) → llcE_out_ag(0, [])
U13_ga(X1, llcA_out_ga(X1, X3)) → llcA_out_ga(s(X1), .(X3))
selectcB_in_aga(.(X3)) → U14_aga(X3, selectcB_in_aga(X3))
selectcB_in_aga(.(X2)) → selectcB_out_aga(.(X2), X2)
U21_aaga(X3, selectcB_out_aga(X3, X4)) → selectcD_out_aaga(X3, .(X4))
U14_aga(X3, selectcB_out_aga(X3, X4)) → selectcB_out_aga(.(X3), .(X4))
U19_ag(X3, llcE_out_ag(X1, X3)) → llcE_out_ag(s(X1), .(X3))
(34) Obligation:
Q DP problem:
The TRS P consists of the following rules:
TC_IN_G(s(X1)) → U6_G(X1, llcA_in_ga(X1))
U8_G(X1, selectcD_out_aaga(X2, X5)) → U10_G(X1, llcE_in_ag(X5))
U10_G(X1, llcE_out_ag(X6, X5)) → TC_IN_G(X6)
The TRS R consists of the following rules:
llcA_in_ga(s(X1)) → U13_ga(X1, llcA_in_ga(X1))
llcA_in_ga(0) → llcA_out_ga(0, [])
U13_ga(X1, llcA_out_ga(X1, X3)) → llcA_out_ga(s(X1), .(X3))
selectcD_in_aaga(X3) → U21_aaga(X3, selectcB_in_aga(X3))
selectcB_in_aga(.(X3)) → U14_aga(X3, selectcB_in_aga(X3))
selectcB_in_aga(.(X2)) → selectcB_out_aga(.(X2), X2)
U14_aga(X3, selectcB_out_aga(X3, X4)) → selectcB_out_aga(.(X3), .(X4))
U21_aaga(X3, selectcB_out_aga(X3, X4)) → selectcD_out_aaga(X3, .(X4))
selectcD_in_aaga(X2) → selectcD_out_aaga(X2, X2)
llcE_in_ag(.(X3)) → U19_ag(X3, llcE_in_ag(X3))
llcE_in_ag([]) → llcE_out_ag(0, [])
U19_ag(X3, llcE_out_ag(X1, X3)) → llcE_out_ag(s(X1), .(X3))
The set Q consists of the following terms:
llcA_in_ga(x0)
U13_ga(x0, x1)
selectcD_in_aaga(x0)
selectcB_in_aga(x0)
U14_aga(x0, x1)
U21_aaga(x0, x1)
llcE_in_ag(x0)
U19_ag(x0, x1)
We have to consider all (P,Q,R)-chains.
(35) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 3 less nodes.
(36) TRUE